COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00005 ENDMK
C⊗;


					Oct 2,1973





Dr. Donald W. Loveland
Computer Science Department
Duke University
Durham, North Carolina  27706


Dear Dr. Loveland:


Here finally are the examples.  Jorge had hoped to extend his Geometry
results but they are more difficult than he first expected. Even at that
his partial results are good examples of interactive theorem proving.
I hope they were worth waiting for.

The times on all of these examples are not best possible since the program
usually picked its own strategies. Jorge's strategy selections were based
mostly on mathematical grounds rather than on attempts to minimize time.

The choice strategies generated by the program in the examples are
ancestry filter with a support set being the negation of the theorem (THM).
The generated editing strategies are of the form: DEPTH[n]∨LENGTH[m], which
means discard any clauses whose depth of function-nesting is greater than
n or whose literal count exceeds m.

The proof print-out is abbreviated.  An auxiliary rule of inference called
`unit-reduction' is used to simplify clauses before they are added to the
memory. Unit-reduction works as follows: let P(t) be a literal in a newly
generated clause; if there already exits a unit of the form ¬P(t1) and
a substitution α such that α⊗t1=t then the literal P(t) is removed from
the new clause. Applications of unit-reduction are not (yet) shown in the
proof tree. This sometimes makes the proofs a bit obscure.

I am enclosing the latest copy of the documentation of the prover. As you
probably know we are current interested in developing a system in which a user
can state his problem and his hunches about how the proof might go, what 
are interesting deductions and other useful information. The current system
reflects only a very simple beginning.


					Sincerely yours,



					John Allen